/**
 * 
 */
package extensionTools.smvCreator;

import java.util.ArrayList;
import java.util.Dictionary;
import java.util.Enumeration;
import java.util.HashSet;
import java.util.Set;

import extensionTools.smvCreator.Link.LinkType;
import extensionTools.smvCreator.Link.SmvType;

import extensionTools.smvCreator.Exceptions.RulesUtilsException;
import extensionTools.smvCreator.Exceptions.SmvCreatorException;
import extensionTools.smvCreator.Exceptions.SmvDBException;
import extensionTools.smvCreator.Exceptions.SmvInputException;
/**
 * @author dani
 *
 */
public class EvObjects extends Rule {

        public EvObjects(DiagramDatabase db) {
                super(db);
            
        }

        /**
         * This function receives a database and creates the rules regarding object
         * creation/consumption and object state modify. 
         * @param db the system's Database
         * @return A String in SMV which implements the rule
         * @throws SmvCreatorException 
         */
        @Override
        public String createRule() throws SmvCreatorException {
                ArrayList<SmvObject> objects = db.getSmvObjectList();
                String rule = "";
                for (SmvObject obj : objects) {
                   	    ArrayList<String[]> returnCaseLines = new ArrayList<String[]>();
                        if(obj.isEnvironmental()){
                        	for (int i=0; i<SMVCreator.K; i++)
                        	{

                        		returnCaseLines.add(environmentalCreation(obj , db,i));             
                        	}
                        }

                        ArrayList<Link> links = obj.getLinkList();
                       	ArrayList<Link> modifyByLabel = new ArrayList<Link>();
                       	ArrayList<Link> modifyByEffect = new ArrayList<Link>();
                       	ArrayList<Link> consumptionLinks = new ArrayList<Link>();
                        //init's consumption,result and modify links
                        for (Link link : links) {
                        	//regular consumption of object by process
                        	if(link.getLinkType() == LinkType.CONSUMPTION &&  link.getLabel() == "")
                        	{
                        		
                        		rule += consumptionLinks(link,obj);
                        		consumptionLinks.add(link);
                        	}
                        	
                        	ArrayList<State> checkStates = obj.getStateList();
                        	//ev_modify object by process with labeled links
                        	if ((//link.getLinkType() == LinkType.RESULT  || 
                        		 link.getLinkType() == LinkType.CONSUMPTION) 
                        		 && link.getLabel() != "" && checkStates != null)
                        	{
                        		rule += "\n" + normalModify(obj , db,link);
                        		modifyByLabel.add(link);
                        	}
                        	//ev_modify object by process with EFFECT link
                            if (link.getLinkType() == LinkType.EFFECT && checkStates != null 
                            										&& checkStates.size() > 1)
                            {
                            	rule += "\n" + effectModify(obj , db,link);
                            	modifyByEffect.add(link);
                            }
                            //Object creation
                            if ((link.getLinkType() == LinkType.RESULT && link.getLabel() == "") 
                            || (link.getLinkType() == LinkType.RESULT 
                            && link.getDstType() == SmvType.OBJECT))
                            {
                            	for (int i=0; i<SMVCreator.K; i++)
                            	{
                            		if (returnCaseLines.size()<SMVCreator.K)
                            		{
                            			returnCaseLines.add(normalCreation(obj , db,link,i));
                            		}
                            		else
                            		// if there is more than two result links into the object then
                            		// we will add the case line for the new link to a place
                            		// in the array link corresponding to it instance
                            		//[[link1_0 case lines ,link2_0 case lines ,  .. ],[link1_1 case lines...]...]
                            		//this way the size of the ArrayList will never be more than k
                            		{
                            			returnCaseLines.set(i,RulesUtils.combineStrings
                            			(returnCaseLines.remove(i),normalCreation(obj , db,link,i)));
                            		}
                            	}
                            	
                            }                        	
                           }
                        int i = 0;
                        String objName = obj.getName();

                        if (returnCaseLines.isEmpty())
                        {
                        	for (;i<SMVCreator.K;i++)
                        	{
                            	String[] caseLines = null;
                            	caseLines = RulesUtils.combineStrings(caseLines,
                            			objectConsumptionLines(obj,consumptionLinks,i));
                            	caseLines=RulesUtils.combineStrings(caseLines,
                            			objectModifyLines(obj,modifyByLabel,modifyByEffect,i));
                            	caseLines=RulesUtils.addDefaultState(caseLines,"TRUE",
                                        obj.getName()+"_"+i);
                            	
                                rule += SmvOp.next(objName+"_"+i,
                                        SmvOp.createCase(caseLines) );
                        	}
                      
                        }
                        else
                        {
                        //for object modify and default links
                        	for (String[] caseLines : returnCaseLines)
                        	{
                            	caseLines = RulesUtils.combineStrings(caseLines,
                            			objectConsumptionLines(obj,consumptionLinks,i));
                            	caseLines=RulesUtils.combineStrings(caseLines,
                            			objectModifyLines(obj,modifyByLabel,modifyByEffect,i));
                            	caseLines=RulesUtils.addDefaultState(caseLines,"TRUE",
                                        obj.getName()+"_"+i);
                            	
                                rule += SmvOp.next(objName+"_"+i,
                                        SmvOp.createCase(caseLines) );
                                i++;
                        	}
                        }
                }
                return rule;
        }

		private String[] environmentalCreation(SmvObject obj,
				DiagramDatabase db, int i) throws RulesUtilsException {
			
			RulesUtils.checkParamsForNull(obj,db);
			
			String initialState = "";
			State  initState = obj.getInitialState();
			if (null != initState)
			{
				initialState = "_" + initState.getName();
			}

			String name = "ev_create_"+obj.getName()+"_"+i+initialState;
			String[] caseLines = new String[1];
			ArrayList<State> states = obj.getStateList();
			State state = obj.getInitialState();
			if (state == null)
			{
				if (states.isEmpty())
				{
					caseLines[0] = SmvOp.createCaseLine(SmvOp.and("sysState = step1",
	              	  		obj.getName()+"_"+i+"=notExist",name+"=0"), 
	              	  		"exist");
				}
				else
				{
					String statesInit =RulesUtils.getStateNames(obj);  
                    //choose initial state randomly
                    String nextValue = statesInit.substring(0,
                                    statesInit.indexOf(",notExist"));
                    nextValue = "{"+nextValue+"}";
					caseLines[0] = SmvOp.createCaseLine(SmvOp.and("sysState = step2",
	              	  		obj.getName()+"_"+i+"=notExist",name+"=0"), 
	              	  	nextValue);
				}
			}
			else
			{
				caseLines[0] = SmvOp.createCaseLine(SmvOp.and("sysState = step2",
              	  		obj.getName()+"_"+i+"=notExist",name+"=0"), 
              	  	state.getName());
			}

			return caseLines;
		}

		/**
         * This function creates the case for all consumption link of the object
         * @param link
         * @return a rule for the consumption
         * @throws SmvDBException - in case of some bad DB behavior
         * @throws SmvInputException - when input doesn't follow the assumptions (like in case of a link 
         * 							   between the uppermost process to some object
		 * @throws RulesUtilsException - when null parameters were sent to SmvOp
         */
        private String consumptionLinks(Link link,SmvObject obj) throws SmvDBException, SmvInputException, RulesUtilsException {
			String conRule = "";
			long src = link.getSrcId();
			long dst = link.getDstId();
			SmvProcess proc = RulesUtils.getProccessbyId(dst, db);
			//verify the link's sanity
			if(proc == null) throw new SmvDBException("EvObjects: no process found at end of a consumption link: " + link.getDstType());
			State s = null;
			if(link.getSrcType() == SmvType.STATE){
				s = obj.idBelongsToObj(src);	
				if(s == null) throw new SmvDBException("EvObjects: unexpected object or state in link " + link.getSrcType());
			}
			//if s is null at this point, the consumption if without a state
			for(int i = 0 ; i<SMVCreator.K; i++)
				for(int j = 0; j<SMVCreator.K; j++){
					String linkName;
					if(s==null) linkName = "ev_consumption_"+obj.getName()+"_"+i+"_"+proc.getName()+"_"+j;
					else linkName = "ev_consumption_"+obj.getName()+"_"+i+"_"+s.getName()+"_"+proc.getName()+"_"+j;
					SmvProcess father = RulesUtils.getProccessbyId(proc.getFatherId(),db);
					if(father == null) throw new SmvInputException("EvObjects: tried to find the father of: "+proc.getName()+" who doesn't exist");
					//if there's an assoc link of consumption between the object and the process father
					String ruleLines[] = new String[3];
					ruleLines[0] = SmvOp.createCaseLine(SmvOp.and("assoc_"+obj.getName()+"_"+i+"_"+father.getName()+"_"+j+ "=TRUE","ev_activate_"+proc.getName()+"_"+j +"=TRUE",
														"sysState = event2"),"TRUE");
					ruleLines[1] = SmvOp.createCaseLine(SmvOp.and("sysState = event2",linkName+ "= TRUE"), "FALSE");
					ruleLines[2] = SmvOp.createCaseLine("TRUE", linkName);
					conRule += SmvOp.next(linkName,SmvOp.createCase(ruleLines)); 
			}
			return conRule;
		}
     
        /**
         * This function creates the case for all modify links of the object
         * @param obj - the Object
         * @param db  - The Database
         * @return a rule for the result Link
         * @throws SmvDBException - in case of some bad DB behavior
         * @throws SmvInputException - when input doesn't follow the assumptions (like in case of a link 
         * 							   between the uppermost process to some object
         * @throws RulesUtilsException 
         */	
        private String normalModify(SmvObject obj, DiagramDatabase db, Link lnk) throws SmvDBException, 
        SmvInputException, RulesUtilsException {
        	RulesUtils.checkParamsForNull(obj,db,lnk);
			
			String returnRule = "";
            int k = SMVCreator.K;
            String objName = obj.getName();
            if (lnk.getDstId() == obj.getId() || lnk.getSrcId() == obj.getId())
    		{
    			throw new SmvDBException("EvObjects: a source or a destination of a " +
    					"labeled link"+ lnk+" cannot be an Object only his states " +
    							"or a Process" );
    		}

    		State dstState = obj.idBelongsToObj(lnk.getDstId());
        	SmvProcess proc = null;
       		State nextState = null;
    
        	if (lnk.getSrcType() == SmvType.PROCESS)
        	{
        		return "";
        	}
        	else //source of the link is one of object states
        	{
        		proc = RulesUtils.getProccessbyId(lnk.getDstId(), db);
        		dstState = obj.idBelongsToObj(lnk.getSrcId());
        		nextState = obj.idBelongsToObj(dstState.getDestStateId().get(lnk.getLabel()));
        	}
        	//the state that is the source of the link have a next state
    		if (nextState != null)
    		{
    			SmvProcess father = RulesUtils.getProccessbyId(proc.getFatherId(),db);
				if(father == null){
					throw new SmvInputException("EvObjects: tried to find the " +
						"father of: "+proc.getName()+" who doesn't exist");
				}	
				ArrayList<State> states = new ArrayList<State>();
				states.add(dstState);
				states.add(nextState);
				for (int i=0; i<k; i++){
					for (int j =0 ;j<k; j++)
					{
                	    returnRule += createModifyCase(objName+"_"+i,proc.getName()+"_"+j,
                	    	father.getName()+"_"+j,states,
                	    	lnk.getLabel())+"\n";
            		}
            	}            	
            	
            }
			return returnRule;
		}
        /**
         * This function creates the case for modify bidirectional link
         * @param obj - the Object
         * @param db  - The Database
         * @param lnk - the EFFECT link to/from an object 
         * @return a rule for the modify
         * @throws SmvDBException - in case of some bad DB behavior
         * @throws RulesUtilsException - in case one of the parameters is a null parameter
         * @throws SmvInputException - when input doesn't follow the assumptions (like in case of a link 
         * 							   between the uppermost process to some object
         */	
		private String effectModify(SmvObject obj, DiagramDatabase db,Link lnk) 
		throws SmvDBException, RulesUtilsException, SmvInputException {
			RulesUtils.checkParamsForNull(obj,db,lnk);
			String returnRule = "";
            int k = SMVCreator.K;
    
            String objName = obj.getName();
            if (RulesUtils.getObjectbyId(lnk.getSrcId(),db).getName() != objName )
    		{
    			throw new SmvDBException("EvObjects: The EFFECT link that passed to this function" +
    					"does not point to" + objName);
    		}

            ArrayList<State> states =obj.getStateList();

            if (states == null || states.size() < 2)
            {
            	return "";
            }
    		SmvProcess proc = RulesUtils.getProccessbyId(lnk.getDstId(), db);
    		SmvProcess father = RulesUtils.getProccessbyId(proc.getFatherId(),db);
    		
    		for (int i=0; i<k; i++){
				for (int j =0 ;j<k; j++)
				{
            	    returnRule += createModifyCase(objName+"_"+i,proc.getName()+"_"+j,
            	    father.getName()+"_"+j,states)+"\n";
        		}
        	}   
			
			return returnRule;
		}

		/**
         * This function creates the case for all RESULT links of the object, include the links that
         * are part of a XOR/OR link
         * @param obj - the Object
         * @param db  - The Database
         * @return a rule for the result Link
         * @throws SmvDBException - in case of some bad DB behavior
		 * @throws RulesUtilsException 
         * @throws SmvInputException - when input doesn't follow the assumptions (like in case of a link 
         * 							   between the uppermost process to some object
         */		
		private String[] normalCreation(SmvObject obj, DiagramDatabase db,Link lnk, int i) 
		throws SmvDBException,RulesUtilsException, SmvInputException {
			
			RulesUtils.checkParamsForNull(obj,db,lnk);
			
            String states ="";
            long dstId = lnk.getDstId();                         
            
            /*
            //its an effect link but from a process to a object state, we will use link 
            //twin brother from the object state to the process
            if(lnk.getLinkType() != LinkType.EFFECT  && 
            		lnk.getLabel() != "" && lnk.getDstType() == SmvType.STATE)

            {
            	return returnCaseLines;
            }     */
          
            //the object is the destination of the link
            if (dstId == obj.getId())
            { 

            	State  initState = obj.getInitialState();
                //no initial state so we will randomly pick the next state;
                if(initState == null && obj.getStateList().size() > 0){
                	states =RulesUtils.getStateNames(obj);                                  
                 }
                if (initState != null)
                {
                	states = initState.getName();   
                }
            }
            else
            {
            	//find if the link destination was one of the object states
            	State dstState = obj.idBelongsToObj(dstId);
                if(null != dstState) 
                {
                	states = dstState.getName();
                }
                //Result link with label == modify link
                else
                {
                	if (lnk.getLinkType() != LinkType.EFFECT)
                	{
                		throw new SmvDBException("EvObjects: A link:"+ lnk + " " +
                				"that belongs to Object"+ obj.getName()
                				+"and her source is a process do not point to and Object " +
            					 "or to one of its " +"states");
                	}
                }
            }

        	String[] returnCaseLines = null;
            String objName = obj.getName();
            String processName = db.getProcessNameById(lnk.getSrcId());

            //see if the link is part of a XOR connection with other link, and if so with whom
            ArrayList<Link> currXorList= RulesUtils.lnkInXor(db,lnk);
            if ( currXorList != null)
            {                              
            	returnCaseLines=RulesUtils.combineStrings(returnCaseLines,
                CreateXorObjectWithStates(objName,processName,states,
                		currXorList,true, i));
            }
            else
            {
            	//see if the link is part of a OR  connection with other link, and if so with whom
            	ArrayList<Link> currOrList= RulesUtils.lnkInOr(db,lnk);
                if (currOrList != null)
                {
                	returnCaseLines=RulesUtils.combineStrings(returnCaseLines,
                    CreateXorObjectWithStates(objName,processName,
                    		states,currOrList,false, i));
                }
                //regular link
                else
                {

                returnCaseLines=RulesUtils.combineStrings(returnCaseLines,
                                CreateObjectWithStates(objName, 
                processName,states, i));
                }
            }  
            
            return returnCaseLines;				
                
}
        



        
		/**
         * This function creates the case for all RESULT links of the object that are part
         * are part of a XOR/OR 
         * @param objName - object name
         * @param processName  - process name that have a RESULT link to the object named objName
         * @param states - the initial state that the object will start with. If the object doesn't 
         * 				   have an initial state then, "states" will hold all object states.
         * 				   If object doesn't have states at all , "states"="".
         * @param currXorList - all the links that are in a XOR/OR with a result link connecting
         * 						processName and objName.
         * @param orXor - boolean telling if this connection by RESULT link, is part of a XOR or OR
         * 				  true- is for XOR. false- is for OR.
         * @return rules lines for the creation by RESULT Link in XOR/OR.
         * @throws SmvDBException - in case of some bad DB behavior
		 * @throws RulesUtilsException - exception of RulesUtils class
         */		
        private String[] CreateXorObjectWithStates(String objName,
                        String processName, String states, ArrayList<Link> currXorList,
                        boolean orXor, int currPlace) 
        				throws RulesUtilsException, SmvDBException {
        	
                ArrayList<String> objs = null;
                Enumeration<String> keys = null;
                Dictionary<String, String> evXors = null; 
                String currObjName = objName + "_"+currPlace;
                String nextValue = states;
                objs = RulesUtils.getDstNames(currXorList,db);
                
                evXors = RulesUtils.getXorDict(processName, objs, orXor);
                keys = evXors.keys();

                if (states == "")
                {
                        currObjName = objName + "_"+currPlace;
                        nextValue = "exist";
                }
                if (states.endsWith("notExist"))
                {
                        nextValue = states.substring(0,
                                        states.indexOf(",notExist"));
                        nextValue = "{"+nextValue+"}";
                }
                int k = SMVCreator.K;
                //calculate the number of permutations of all object in XOR k^numObjs
                int numPermutation=(int) Math.pow(k,objs.size());
                if (orXor == false)
                {		//the number of lines needed for the OR rule
                        numPermutation =numPermutation* (int)( Math.pow(2,objs.size()) -
                        		Math.pow(2,objs.size()-1));
                }
             
                String[] caseExist = new String[numPermutation];
                int i =0;
                
                while (keys.hasMoreElements()) {
                    
                    String currEventName = keys.nextElement();
                    if (currEventName.contains(currObjName))
                    {
                    	//link is in OR connection
                    	if (false == orXor )
                    	{
                            String[] elem = evXors.get(currEventName).split(",");
                            for (String elm : elem)
                            {
                                    if (elm.contains(currObjName))
                                    {
                                            caseExist[i] = SmvOp.createCaseLine
                                            (SmvOp.and("sysState = step2 ",
                                            currEventName+"="+elm),nextValue);
                                            i++;
                                    }
                            }
                    	} 
                    	//XOR
                    	else
                        {
                                caseExist[i] = SmvOp.createCaseLine(SmvOp.and
                                                ("sysState = step2 ",currEventName+"="+currObjName+"_"), 
                                                nextValue);
                                i++;
                        }                            
                    }
            }                        
               
     return caseExist;
  }
        
        /**
         * This function create the rule lines regarding object modification from one state to another.
         * This function deals with both modification links, RESULT with label or EFFECT link
         * @param obj - the object to modify
         * @param modifyByLabel  - list of links that modify the object "obj" with labeled RESULT links
         * @param modifyByEffect - list of links that modify the object "obj" with effect links.
         * @param instance - the instance of the object that we are creating the rule for.
         * @return rule lines for the modification of the object.
         * @throws SmvCreatorException
         */
        private String[] objectModifyLines(SmvObject obj, ArrayList<Link> modifyByLabel,
      		  ArrayList<Link> modifyByEffect, int instance) throws SmvCreatorException {
      	  
      	  if (modifyByLabel.isEmpty() && modifyByEffect.isEmpty())
        	{
        		return null;
        	}
        	ArrayList<String> modifyCaseLines = new ArrayList<String>();
        	String objName = obj.getName();
        	ArrayList<State> objStates= obj.getStateList();
        	//going over all labeled modify links that their source is a state
        	for (Link lblLink : modifyByLabel)
            {
      			State dstState = obj.idBelongsToObj(lblLink.getSrcId());
      			State nextState = obj.idBelongsToObj(dstState.getDestStateId()
      													.get(lblLink.getLabel()));
        		if (nextState == null)
        		{
        			continue;
        		}
      			if (!(objStates.contains(obj.idBelongsToObj(lblLink.getSrcId()))))
      			{
      				throw new SmvCreatorException("EvObjects: The source of a moodify Label link with Label" 
      						+"is not one of the Object: "+objName+" states");
      			}
      			String processName = db.getProcessNameById(lblLink.getDstId());

        		for (int j=0 ; j < SMVCreator.K;j++ )
        		{
        			String next = "ev_modify_"+objName+"_"+instance+"_"
        						  +processName+"_"+j+"_"+dstState.getName()+
        						  "_"+nextState.getName();
        			modifyCaseLines.add(SmvOp.createCaseLine(SmvOp.and("sysState = step2 ",
                        		next+"= TRUE"), nextState.getName()));
        		}
            }
        	
        	//going over all effect links from an object, and only if an object has more than
        	// one state, because otherwise there is nothing to effect
        	for (Link effLink : modifyByEffect)
        	{
      			if (obj.getId() != effLink.getSrcId())
      			{
      				throw new SmvCreatorException("EvObjects: The source of a EFFECT  link " 
      						+"is not the Object: "+objName+" tha was given as a parameter");
      			}
      			String processName = db.getProcessNameById(effLink.getDstId());
      				Set<State> newSet = new HashSet<State>(objStates);
      			for (State state: objStates)
      			{
      				Set<State> singleState = new HashSet<State>();
      				singleState.add(state);
      				//find states\states[i]
      				Set<State> otherStates = RulesUtils.diffrenceSet(newSet, singleState) ;
      				ArrayList<String> statesNames = new ArrayList<String>();
      				//create an array list of all possible state names , for ev_modify next
      				for (State currState: otherStates)
      				{
      					statesNames.add(currState.getName());
      				}
      				for (int j=0 ; j < SMVCreator.K;j++ )
      				{
            			String next = "ev_modify_"+objName+"_"+instance+"_"
      				  					+processName+"_"+j+"_"+state.getName();
            			modifyCaseLines.add(SmvOp.createCaseLine(SmvOp.and("sysState = step2 ",
            			 next+"= TRUE"), SmvOp.prepareBrackets(statesNames)));
      				}
      			}
        		}
        		

      		return RulesUtils.arrayListToArray(modifyCaseLines);
      }      	
  
        /**
         * This function create the rule lines regarding object consumption
         * @param obj - the object to consume
         * @param modifyByLabel  - list of links that the object may be consumed by.
         * @param instance - the instance of the object that we are creating the rule for.
         * @return rule lines for the modification of the object.
         * @throws SmvCreatorException
         */      	
        
		private String[] objectConsumptionLines(SmvObject obj,
				ArrayList<Link> consumptionLinks, int instance) throws SmvCreatorException {
			

			if (consumptionLinks.isEmpty())
        	{
        		return null;
        	}
			
        	String objName = obj.getName();
			if (consumptionLinks.size() > 1)
			{
				throw new SmvCreatorException("EvObjects: There cannot be more than one consumption links to a single " +
						"Object. and Object : "+objName+" has more than one");
			}
        	ArrayList<String> consumptionCaseLines = new ArrayList<String>();

        	Link link = consumptionLinks.get(0);
        	State srcState = null;
        	String processName = db.getProcessNameById(link.getDstId());
			String check = "ev_consumption_"+obj.getName()+"_"+instance+"_"+processName;
        	//link from state of the object
        	if (link.getSrcType() == SmvType.STATE)
        	{
        		srcState = obj.idBelongsToObj(link.getSrcId());
    			if (!(obj.getStateList().contains(obj.idBelongsToObj(srcState.getId()))))
    			{
    				throw new SmvCreatorException("EvObjects: The source of consumption link " 
    						+"is not one of the Object: "+objName+" states");
    			}
    			check = "ev_consumption_"+obj.getName()+"_"+instance+"_"+srcState.getName()+
    			"_"+processName;
        	}
        	
        	
        	for (int i=0 ; i < SMVCreator.K;i++ )
			{

    			consumptionCaseLines.add(SmvOp.createCaseLine(SmvOp.and("sysState = step2 ",check+"_"+i+"=TRUE"
    			 ) , "notExist"));
			}
        	return RulesUtils.arrayListToArray(consumptionCaseLines);
		}
   
        /**
         * This function create the rule lines regarding object creation
         * @param objName - object name
         * @param processName  - process name that have a RESULT link to the object named objName
         * @param states - the initial state that the object will start with. If the object doesn't 
         * 				   have an initial state then, "states" will hold all object states.
         * 				   If object doesn't have states at all , "states"="".
         * @param currPlace - the instance of the object that we are creating the rule for.
         * @return rule lines for the creation of the object.
         * @throws SmvInputException 
         * @throws RulesUtilsException - when null parameters were sent to SmvOp
         */     
		private String[] CreateObjectWithStates(String objName, String processName,
                String states, int currPlace) throws SmvInputException, RulesUtilsException {
			
        	if(objName == "" || processName == "")
        	{
        		throw new SmvInputException("EvObjects: one of the parameters for createModifyCase is empty");
        	}
        	String currObjName = objName + "_"+currPlace;
        	String nextValue = states;
        	String firstState = "_"+states;
        	if (states == "" )
            {
                    currObjName = objName + "_"+currPlace;
                    nextValue = "exist";
                    firstState = "";
            }
            if (states.endsWith("notExist"))
            {
                    
                    nextValue = states.substring(0,
                                    states.indexOf(",notExist"));
                    nextValue = "{"+nextValue+"}";
                    firstState="";
            }
            
            int k = SMVCreator.K;
            String[] caseExist = new String[k];
            for (int i=0 ; i<k; i++){
                            caseExist[i] = SmvOp.createCaseLine(SmvOp.and("sysState = step2 ",
                                            "ev_create"+"_"+processName+"_"+i+"_"+currObjName+
                                            firstState+"=TRUE"), 
                                            nextValue);
            }
            return caseExist;
    }		
        
                
        /**
         * This function create the ev_modify case for links with label on them
         * * @param objName - object name
         * @param processName  - process name that have a RESULT link to the object named objName
         * @param fatherName - father name of the process that is modifying.
         * @param states - the object that is named "objName" names.
         * @param path - the label on the RESULT link that modifies the object.
         * @return The case as a string
         * @throws SmvInputException - in case invalid parameters for ev_modify
         * @throws RulesUtilsException 
         */

        private String createModifyCase(String objName, String processName, String fatherName,
				ArrayList<State> states, String path) throws SmvInputException, RulesUtilsException {
        	
        	if(fatherName == "" || objName == "" || processName == "" || states == null)
        	{
        		throw new SmvInputException("EvObjects: one of the parameters for createModifyCase is empty");
        	}
			String caseMod[] = new String[3];
	    	String ev_name = "ev_modify_"+objName+"_"+processName+"_"+states.get(0).getName()+
			"_"+states.get(1).getName();
			
			caseMod[0] = SmvOp.createCaseLine(SmvOp.and("sysState = event2 ",
					objName +"="+states.get(0).getName(), "ev_terminate_"+processName+"=0",
					"assoc_"+fatherName+"_"+objName+"=TRUE"), 
					"TRUE");
			
			caseMod[1] = SmvOp.createCaseLine("sysState = event2 ", "FALSE");
			caseMod[2] = SmvOp.createCaseLine("TRUE ", ev_name);
			


			return SmvOp.next(ev_name,SmvOp.createCase(caseMod));
		}
        
        /**
         * This function create the ev_modify event case for EFFECT links
         * @param objName - object name
         * @param processName  - process name that have a RESULT link to the object named objName
         * @param fatherName - father name of the process that is modifying.
         * @param states - the object that is named "objName" names.
         * @return The case as a string
         * @throws SmvInputException - in case invalid parameters for ev_modify
         * @throws RulesUtilsException 
         */
        
        private String createModifyCase(String objName, String processName, String fatherName,
				ArrayList<State> states) throws SmvInputException, RulesUtilsException 
		{
        	if(fatherName == "" || objName == "" || processName == "" || states == null)
        	{
        		throw new SmvInputException("EvObjects: one of the parameters for createModifyCase is empty");
        	}
			String caseMod[] = new String[3];			
			String returnRule = "";
			int numberOfStates = states.size();
			
			//create a case for every state where the other states are the next
			for (int i = 0 ; i<numberOfStates;i++)
			{
				String sourceStateName = states.get(i).getName();
				String ev_name = "ev_modify_"+objName+"_"+processName+"_"+sourceStateName;

				caseMod[0] = SmvOp.createCaseLine(SmvOp.and("sysState = event2 ",
						objName +"="+sourceStateName, "ev_terminate_"+processName+"=0",
						"assoc_"+fatherName+"_"+objName+"=TRUE"), 
						"TRUE");
				
				caseMod[1] = SmvOp.createCaseLine("sysState = event2 ", "FALSE");
				caseMod[2] = SmvOp.createCaseLine("TRUE ", ev_name);
				
				returnRule += SmvOp.next(ev_name,SmvOp.createCase(caseMod));
			}
			
			return returnRule;
		}
}
